{-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-}
{-# Language OverloadedStrings #-}
{-# Language Safe #-}
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Cryptol.TypeCheck.Error where

import qualified Data.IntMap as IntMap
import qualified Data.List.NonEmpty as NE
import qualified Data.Set as Set
import Control.DeepSeq(NFData)
import GHC.Generics(Generic)
import Data.List((\\),sortBy,partition)
import Data.Function(on)

import Cryptol.Utils.Ident(Ident,Namespace(..))
import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Position(Located(..), Range(..), rangeWithin)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Subst
import Cryptol.TypeCheck.Unify(Path,isRootPath)
import Cryptol.TypeCheck.FFI.Error
import Cryptol.ModuleSystem.Name(Name)
import Cryptol.Utils.RecordMap

-- | Clean up error messages by:
---  * only reporting one error (most severe) for any given source location
--   * sorting errors by source location (they are accumulated in
--     reverse order by 'recordError')
--   * dropping any errors that are subsumed by another
cleanupErrors :: [(Range,Error)] -> [(Range,Error)]
cleanupErrors = dropErrorsFromSameLoc
              . sortBy (compare `on` (cmpR . fst))    -- order errors
              . dropSubsumed []
  where

  -- pick shortest error from each location.
  dropErrorsFromSameLoc = concatMap chooseBestError
                        . NE.groupBy ((==)    `on` fst)

  addErrorRating (r,e) = (errorImportance e, (r,e))
  chooseBestError    = NE.toList
                     . fmap snd
                     . NE.head
                     . NE.groupBy1 ((==) `on` fst)
                     . NE.sortBy (flip compare `on` fst)
                     . fmap addErrorRating


  cmpR r  = ( source r    -- First by file
            , from r      -- Then starting position
            , to r        -- Finally end position
            )

  dropSubsumed survived xs =
    case xs of
      err : rest ->
         let keep e = not (subsumes err e)
         in dropSubsumed (err : filter keep survived) (filter keep rest)
      [] -> survived

-- | Clean up warning messages by sorting them by source location
--   (they are accumulated in reverse order by 'recordWarning').
cleanupWarnings :: [(Range,Warning)] -> [(Range,Warning)]
cleanupWarnings = 
  sortBy (compare `on` (cmpR . fst))    -- order warnings
  where
    cmpR r  = ( source r    -- First by file
              , from r      -- Then starting position
              , to r        -- Finally end position
              )

-- | Should the first error suppress the next one.
subsumes :: (Range,Error) -> (Range,Error) -> Bool
subsumes (_,NotForAll _ _ x _) (_,NotForAll _ _ y _) = x == y
subsumes (r1,UnexpectedTypeWildCard) (r2,UnsupportedFFIType{}) =
  r1 `rangeWithin` r2
subsumes (r1,KindMismatch {}) (r2,err) =
  case err of
    KindMismatch {} -> r1 == r2
    _               -> True
subsumes (_, TooManyParams nm1 _ _ _) (_, TypeMismatch (DefinitionOf nm2) _ _ _) =
  nm1 == nm2
subsumes _ _ = False

data Warning  = DefaultingKind (P.TParam Name) P.Kind
              | DefaultingWildType P.Kind
              | DefaultingTo !TVarInfo Type
              | NonExhaustivePropGuards Name
              | DuplicateDeriving PC
                deriving (Show, Generic, NFData)

-- | Various errors that might happen during type checking/inference
data Error    = KindMismatch (Maybe TypeSource) Kind Kind
                -- ^ Expected kind, inferred kind

              | TooManyTypeParams Int Kind
                -- ^ Number of extra parameters, kind of result
                -- (which should not be of the form @_ -> _@)

              | TyVarWithParams
                -- ^ A type variable was applied to some arguments.

              | TooManyTySynParams Name Int
                -- ^ Type-synonym, number of extra params

              | TooFewTyParams Name Int
                -- ^ Who is missing params, number of missing params

              | RecursiveTypeDecls [Name]
                -- ^ The type synonym declarations are recursive

              | TooManyParams Name Type Int Int
                -- ^ Name of bind, bind signature, number of patterns given,
                --   expected number of parameters from signature.
                --   More patterns provided for a bind than expected,
                --   given its signature.

              | ClassNotDerivable
                -- ^ Deriving unsupported typeclass
                  Name   -- ^ The thing that the user tried to derive
                  String -- ^ Description of the type declaration
                  [PC]   -- ^ The supported typeclasses for deriving on this
                         --   sort of type declaration

              | DerivingMissingSuperclasses
                -- ^ Deriving instance for a class without deriving instances
                --   for its superclasses
                  PC   -- ^ The class listed in the deriving clause
                  [PC] -- ^ Its superclasses not listed in the deriving clause

              | TypeMismatch TypeSource Path Type Type
                -- ^ Expected type, inferred type

              | EnumTypeMismatch Type
                -- ^ Expected an enum type, but inferred the supplied 'Type'
                --   instead, which is not an enum. This corresponds to the
                --   \"Matched Expression Must Have a Known Enum Type\"
                --   restriction for @case@ expressions, as described in the
                --   Cryptol Reference Manual.

              | SchemaMismatch Ident Schema Schema
                -- ^ Name of module parameter, expected scehema, actual schema.
                -- This may happen when instantiating modules.

              | RecursiveType TypeSource Path Type Type
                -- ^ Unification results in a recursive type

              | UnsolvedGoals [Goal]
                -- ^ A constraint that we could not solve, usually because
                -- there are some left-over variables that we could not infer.

              | UnsolvableGoals [Goal]
                -- ^ A constraint that we could not solve and we know
                -- it is impossible to do it.

              | UnsolvedDelayedCt DelayedCt
                -- ^ A constraint (with context) that we could not solve

              | UnexpectedTypeWildCard
                -- ^ Type wild cards are not allowed in this context
                -- (e.g., definitions of type synonyms).

              | TypeVariableEscaped TypeSource Path Type [TParam]
                -- ^ Unification variable depends on quantified variables
                -- that are not in scope.

              | NotForAll TypeSource Path TVar Type
                -- ^ Quantified type variables (of kind *) need to
                -- match the given type, so it does not work for all types.

              | TooManyPositionalTypeParams
                -- ^ Too many positional type arguments, in an explicit
                -- type instantiation

              | BadParameterKind TParam Kind
                -- ^ Kind other than `*` or `#` given to parameter of
                --   type synonym, newtype, function signature, etc.

              | CannotMixPositionalAndNamedTypeParams

              | UndefinedTypeParameter (Located Ident)

              | RepeatedTypeParameter Ident [Range]

              | AmbiguousSize TVarInfo (Maybe Type)
                -- ^ Could not determine the value of a numeric type variable,
                --   but we know it must be at least as large as the given type
                --   (or unconstrained, if Nothing).

              | BareTypeApp
                -- ^ Bare expression of the form `{_}

              | UndefinedExistVar Name
              | TypeShadowing String Name String
              | MissingModTParam (Located Ident)
              | MissingModVParam (Located Ident)
              | MissingModParam Ident

              | FunctorInstanceMissingArgument Ident
              | FunctorInstanceBadArgument Ident
              | FunctorInstanceMissingName Namespace Ident
              | FunctorInstanceBadBacktick BadBacktickInstance

              | UnsupportedFFIKind TypeSource TParam Kind
                -- ^ Kind is not supported for FFI
              | UnsupportedFFIType TypeSource FFITypeError
                -- ^ Type is not supported for FFI

              | InvalidConstraintGuard Prop
                -- ^ The given constraint may not be used as a constraint guard

              | InvalidConPat Int Int
                -- ^ Bad constructor pattern.
                -- 1) Number of parameters we have,
                -- 2) Number of parameters we need.

              | UncoveredConPat [Name]
                -- ^ A @case@ expression is non-exhaustive and does not cover
                --   the supplied constructor 'Name's.

              | OverlappingPat (Maybe Ident) [Range]
                -- ^ Overlapping patterns in a case

              | TemporaryError Doc
                -- ^ This is for errors that don't fit other cateogories.
                -- We should not use it much, and is generally to be used
                -- for transient errors, which are due to incomplete
                -- implementation.
                deriving (Show, Generic, NFData)

data BadBacktickInstance =
    BIPolymorphicArgument Ident Ident
  | BINested [(BIWhat, Name)]
  | BIMultipleParams Ident
    deriving (Show, Generic, NFData)

data BIWhat = BIFunctor | BIInterface | BIPrimitive | BIForeign | BIAbstractType
    deriving (Show, Generic, NFData)

-- | When we have multiple errors on the same location, we show only the
-- ones with the has highest rating according to this function.
errorImportance :: Error -> Int
errorImportance err =
  case err of
    BareTypeApp                                      -> 11 -- basically a parse error
    TemporaryError {}                                -> 11
    -- show these as usually means the user used something that doesn't work

    FunctorInstanceMissingArgument {}                 -> 10
    MissingModParam {}                                -> 10
    FunctorInstanceBadArgument {}                     -> 10
    FunctorInstanceMissingName {}                     ->  9
    FunctorInstanceBadBacktick {}                     ->  9


    KindMismatch {}                                  -> 10
    TyVarWithParams {}                               -> 9
    TooManyParams{}                                  -> 9
    ClassNotDerivable{}                              -> 8
    DerivingMissingSuperclasses{}                    -> 8
    TypeMismatch {}                                  -> 8
    EnumTypeMismatch {}                              -> 7
    SchemaMismatch {}                                -> 7
    InvalidConPat {}                                 -> 7
    UncoveredConPat {}                               -> 7
    OverlappingPat {}                                -> 3
    RecursiveType {}                                 -> 7
    NotForAll {}                                     -> 6
    TypeVariableEscaped {}                           -> 5

    UndefinedExistVar {}                             -> 10
    TypeShadowing {}                                 -> 2
    MissingModTParam {}                              -> 10
    MissingModVParam {}                              -> 10

    BadParameterKind{}                               -> 9
    CannotMixPositionalAndNamedTypeParams {}         -> 8
    TooManyTypeParams {}                             -> 8
    TooFewTyParams {}                                -> 8
    TooManyPositionalTypeParams {}                   -> 8
    UndefinedTypeParameter {}                        -> 8
    RepeatedTypeParameter {}                         -> 8

    TooManyTySynParams {}                            -> 8
    UnexpectedTypeWildCard {}                        -> 8

    RecursiveTypeDecls {}                            -> 9

    UnsolvableGoals g
      | any tHasErrors (map goal g)                  -> 0
      | otherwise                                    -> 4

    UnsolvedGoals g
      | any tHasErrors (map goal g)                  -> 0
      | otherwise                                    -> 4

    UnsolvedDelayedCt dt
      | any tHasErrors (map goal (dctGoals dt))      -> 0
      | otherwise                                    -> 3

    AmbiguousSize {}                                 -> 2

    UnsupportedFFIKind {}                            -> 10
    UnsupportedFFIType {}                            -> 7
    -- less than UnexpectedTypeWildCard

    InvalidConstraintGuard {}                        -> 5


instance TVars Warning where
  apSubst su warn =
    case warn of
      DefaultingKind {}     -> warn
      DefaultingWildType {} -> warn
      DefaultingTo d ty     -> DefaultingTo d $! (apSubst su ty)
      NonExhaustivePropGuards {} -> warn
      DuplicateDeriving {}  -> warn

instance FVS Warning where
  fvs warn =
    case warn of
      DefaultingKind {}     -> Set.empty
      DefaultingWildType {} -> Set.empty
      DefaultingTo _ ty     -> fvs ty
      NonExhaustivePropGuards {} -> Set.empty
      DuplicateDeriving {}  -> Set.empty

instance TVars Error where
  apSubst su err =
    case err of
      KindMismatch {}           -> err
      TooManyTypeParams {}      -> err
      TyVarWithParams           -> err
      TooManyTySynParams {}     -> err
      TooFewTyParams {}         -> err
      RecursiveTypeDecls {}     -> err
      SchemaMismatch i t1 t2  ->
        SchemaMismatch i !$ (apSubst su t1) !$ (apSubst su t2)
      TooManyParams b t i j     -> TooManyParams b !$ (apSubst su t) .$ i .$ j
      ClassNotDerivable {}      -> err
      DerivingMissingSuperclasses {} -> err
      TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2)
      EnumTypeMismatch t        -> EnumTypeMismatch !$ apSubst su t
      InvalidConPat {}          -> err
      UncoveredConPat {}        -> err
      OverlappingPat {}         -> err
      RecursiveType src pa t1 t2   -> RecursiveType src pa !$ (apSubst su t1) !$ (apSubst su t2)
      UnsolvedGoals gs          -> UnsolvedGoals !$ apSubst su gs
      UnsolvableGoals gs        -> UnsolvableGoals !$ apSubst su gs
      UnsolvedDelayedCt g       -> UnsolvedDelayedCt !$ (apSubst su g)
      UnexpectedTypeWildCard    -> err
      TypeVariableEscaped src pa t xs ->
                                 TypeVariableEscaped src pa !$ (apSubst su t) .$ xs
      NotForAll src pa x t        -> NotForAll src pa x !$ (apSubst su t)
      TooManyPositionalTypeParams -> err
      CannotMixPositionalAndNamedTypeParams -> err

      BadParameterKind{} -> err
      UndefinedTypeParameter {} -> err
      RepeatedTypeParameter {} -> err
      AmbiguousSize x t -> AmbiguousSize x !$ (apSubst su t)

      BareTypeApp -> err

      UndefinedExistVar {} -> err
      TypeShadowing {}     -> err
      MissingModTParam {}  -> err
      MissingModVParam {}  -> err
      MissingModParam {}   -> err

      FunctorInstanceMissingArgument {} -> err
      FunctorInstanceBadArgument {} -> err
      FunctorInstanceMissingName {} -> err
      FunctorInstanceBadBacktick {} -> err

      UnsupportedFFIKind {}    -> err
      UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e

      InvalidConstraintGuard p -> InvalidConstraintGuard $! apSubst su p

      TemporaryError {} -> err


instance FVS Error where
  fvs err =
    case err of
      KindMismatch {}           -> Set.empty
      TooManyTypeParams {}      -> Set.empty
      TyVarWithParams           -> Set.empty
      TooManyTySynParams {}     -> Set.empty
      TooFewTyParams {}         -> Set.empty
      RecursiveTypeDecls {}     -> Set.empty
      SchemaMismatch _ t1 t2    -> fvs (t1,t2)
      TooManyParams _ t _ _     -> fvs t
      ClassNotDerivable {}      -> Set.empty
      DerivingMissingSuperclasses {} -> Set.empty
      TypeMismatch _ _ t1 t2    -> fvs (t1,t2)
      EnumTypeMismatch t        -> fvs t
      InvalidConPat {}          -> Set.empty
      UncoveredConPat {}        -> Set.empty
      OverlappingPat {}         -> Set.empty
      RecursiveType _ _ t1 t2   -> fvs (t1,t2)
      UnsolvedGoals gs          -> fvs gs
      UnsolvableGoals gs        -> fvs gs
      UnsolvedDelayedCt g       -> fvs g
      UnexpectedTypeWildCard    -> Set.empty
      TypeVariableEscaped _ _ t xs-> fvs t `Set.union`
                                            Set.fromList (map TVBound xs)
      NotForAll _ _ x t             -> Set.insert x (fvs t)
      TooManyPositionalTypeParams -> Set.empty
      CannotMixPositionalAndNamedTypeParams -> Set.empty
      UndefinedTypeParameter {}             -> Set.empty
      RepeatedTypeParameter {}              -> Set.empty
      AmbiguousSize _ t -> fvs t
      BadParameterKind tp _ -> Set.singleton (TVBound tp)

      BareTypeApp -> Set.empty

      UndefinedExistVar {} -> Set.empty
      TypeShadowing {}     -> Set.empty
      MissingModTParam {}  -> Set.empty
      MissingModVParam {}  -> Set.empty
      MissingModParam {}   -> Set.empty

      FunctorInstanceMissingArgument {} -> Set.empty
      FunctorInstanceBadArgument {} -> Set.empty
      FunctorInstanceMissingName {} -> Set.empty
      FunctorInstanceBadBacktick {} -> Set.empty

      UnsupportedFFIKind {}  -> Set.empty
      UnsupportedFFIType _ t -> fvs t

      InvalidConstraintGuard p -> fvs p

      TemporaryError {} -> Set.empty

instance PP Warning where
  ppPrec = ppWithNamesPrec IntMap.empty

instance PP Error where
  ppPrec = ppWithNamesPrec IntMap.empty


instance PP (WithNames Warning) where
  ppPrec _ (WithNames warn names) =
    addTVarsDescsAfter names warn $
    case warn of
      DefaultingKind x k ->
        text "Assuming " <+> pp x <+> text "to have" <+> P.cppKind k

      DefaultingWildType k ->
        text "Assuming _ to have" <+> P.cppKind k

      DefaultingTo d ty ->
        text "Defaulting" <+> pp (tvarDesc d) <+> text "to"
                                              <+> ppWithNames names ty

      NonExhaustivePropGuards n ->
        text "Could not prove that the constraint guards used in defining" <+>
        pp n <+> text "were exhaustive."

      DuplicateDeriving pc ->
        "Duplicate" <+> pp pc <+> "in deriving clause"

instance PP (WithNames Error) where
  ppPrec _ (WithNames err names) =
    case err of

      RecursiveType src pa t1 t2 ->
        addTVarsDescsAfter names err $
        nested "Matching would result in an infinite type." $
          vcat ( [ "The type: " <+> ppWithNames names t1
                 , "occurs in:" <+> ppWithNames names t2
                 ] ++ ppCtxt pa ++
                 [ "When checking" <+> pp src ] )

      UnexpectedTypeWildCard ->
        addTVarsDescsAfter names err $
        nested "Wild card types are not allowed in this context" $
          vcat [ "They cannot be used in:"
               , bullets [ "type synonyms"
                         , "FFI declarations"
                         , "declarations with constraint guards"
                         ]
               ]

      KindMismatch mbsrc k1 k2 ->
        addTVarsDescsAfter names err $
        nested "Incorrect type form." $
         vcat $
           [ "Expected:" <+> cppKind k1
           , "Inferred:" <+> cppKind k2
           ] ++ kindMismatchHint k1 k2
             ++ maybe [] (\src -> ["When checking" <+> pp src]) mbsrc

      TooManyTypeParams extra k ->
        addTVarsDescsAfter names err $
        nested "Malformed type."
          ("Kind" <+> quotes (pp k) <+> "is not a function," $$
           "but it was applied to" <+> pl extra "parameter" <.> ".")

      TyVarWithParams ->
        addTVarsDescsAfter names err $
        nested "Malformed type."
               "Type variables cannot be applied to parameters."

      TooManyTySynParams t extra ->
        addTVarsDescsAfter names err $
        nested "Malformed type."
          ("Type synonym" <+> nm t <+> "was applied to" <+>
            pl extra "extra parameter" <.> text ".")

      TooFewTyParams t few ->
        addTVarsDescsAfter names err $
        nested "Malformed type."
          ("Type" <+> nm t <+> "is missing" <+> int few <+> text "parameters.")

      RecursiveTypeDecls ts ->
        addTVarsDescsAfter names err $
        nested "Recursive type declarations:"
               (commaSep $ map nm ts)
      
      TooManyParams n t i j ->
        addTVarsDescsAfter names err $
        nested "Type signature mismatch." $
          vcat $
            [ "Expected number of parameters:" <+> int j
            , "Actual number of parameters:" <+> int i
            , "When defining" <+> quotes ((pp n <> ":") <+> ppWithNames names t) ]

      ClassNotDerivable badCls declDesc allowed ->
        "Cannot derive" <+> backticks (pp badCls) $$
        nested ("Derivable constraints for" <+> text declDesc <+> "declarations are:")
          (commaSepFill (map pp allowed))

      DerivingMissingSuperclasses pc supers ->
        "Missing superclass(es) for" <+> pp pc $$
        "To derive this constraint, you must also derive:" <+>
          commaSepFill (map pp supers)

      TypeMismatch src pa t1 t2 ->
        addTVarsDescsAfter names err $
        nested "Type mismatch:" $
        vcat $
          [ "Expected type:" <+> ppWithNames names t1
          , "Inferred type:" <+> ppWithNames names t2
          ] ++ mismatchHint t1 t2
            ++ ppCtxt pa
            ++ ["When checking" <+> pp src]

      EnumTypeMismatch t ->
        case tNoUser t of
          TVar {} ->
            nested "Failed to infer the type of cased expression."
              "Try giving the expression an explicit type annotation."
          _ ->
            addTVarsDescsAfter names err $
            nested "Type mismatch in cased expresson:" $
              vcat
                [ "Expected: an `enum` type"
                , "Inferred:" <+> ppWithNames names t
                ]

      SchemaMismatch i t1 t2 ->
          addTVarsDescsAfter names err $
          nested ("Type mismatch in module parameter" <+> quotes (pp i)) $
          vcat $
            [ "Expected type:" <+> ppWithNames names t1
            , "Actual type:"   <+> ppWithNames names t2
            ]

      InvalidConPat have need ->
        addTVarsDescsAfter names err $
        nested "Invalid constructor pattern" $
          vcat
            [ "Expected" <+> int need <+> "parameters,"
            , "but there are" <+> int have <.> "."
            ]

      UncoveredConPat conNames ->
        "Case expression does not cover the following patterns:"
        $$ commaSep (map pp conNames)

      OverlappingPat mbCon rs ->
        addTVarsDescsAfter names err $
        nested ("Overlapping choices for" <+> what <.> ":") $
          vcat [ "Pattern at" <+> pp r | r <- rs ]
        where
        what = case mbCon of
                 Just i  -> "constructor" <+> pp i
                 Nothing -> "default case"

      UnsolvableGoals gs -> explainUnsolvable names gs

      UnsolvedGoals gs
        | noUni ->
          addTVarsDescsAfter names err $
          nested "Unsolved constraints:" $
          bullets (map (ppWithNames names) gs)

        | otherwise ->
          addTVarsDescsBefore names err $
          nested "subject to the following constraints:" $
          bullets (map (ppWithNames names) gs)

      UnsolvedDelayedCt g
        | noUni ->
          addTVarsDescsAfter names err $
          nested "Failed to validate user-specified signature." $
          ppWithNames names g
        | otherwise ->
          addTVarsDescsBefore names err $
          nested "while validating user-specified signature" $
          ppWithNames names g

      TypeVariableEscaped src pa t xs ->
        addTVarsDescsAfter names err $
        nested ("The type" <+> ppWithNames names t <+>
                                        "is not sufficiently polymorphic.") $
          vcat ( [ "It cannot depend on quantified variables:" <+>
                       (commaSep (map (ppWithNames names) xs))
                 ] ++ ppCtxt pa
                   ++ [ "When checking" <+> pp src ]
               )

      NotForAll src pa x t ->
        addTVarsDescsAfter names err $
        nested "Inferred type is not sufficiently polymorphic." $
          vcat ( [ "Quantified variable:" <+> ppWithNames names x
                 , "cannot match type:"   <+> ppWithNames names t
                 ] ++ ppCtxt pa
                   ++ [ "When checking" <+> pp src ]
               )

      BadParameterKind tp k ->
        addTVarsDescsAfter names err $
        vcat [ "Illegal kind assigned to type variable:" <+> ppWithNames names tp
             , "Unexpected:" <+> pp k
             ]

      TooManyPositionalTypeParams ->
        addTVarsDescsAfter names err $
        "Too many positional type-parameters in explicit type application."

      CannotMixPositionalAndNamedTypeParams ->
        addTVarsDescsAfter names err $
        "Named and positional type applications may not be mixed."

      UndefinedTypeParameter x ->
        addTVarsDescsAfter names err $
        "Undefined type parameter `" <.> pp (thing x) <.> "`."
          $$ "See" <+> pp (srcRange x)

      RepeatedTypeParameter x rs ->
        addTVarsDescsAfter names err $ nest 2 $
          "Multiple definitions for type parameter `" <.> pp x <.> "`:"
          $$ bullets (map pp rs)

      AmbiguousSize x t ->
        let sizeMsg =
               case t of
                 Just t' -> ["Must be at least:" <+> ppWithNames names t']
                 Nothing -> []
         in addTVarsDescsAfter names err
              (vcat (["Ambiguous numeric type:" <+> pp (tvarDesc x)] ++ sizeMsg))

      BareTypeApp ->
        "Unexpected bare type application." $$
        "Perhaps you meant `( ... ) instead."

      UndefinedExistVar x -> "Undefined type" <+> quotes (pp x)
      TypeShadowing this new that ->
        "Type" <+> text this <+> quotes (pp new) <+>
        "shadowing an existing" <+> text that <+> "with the same name."
      MissingModTParam x ->
        "Missing definition for type parameter" <+> quotes (pp (thing x))
      MissingModVParam x ->
        "Missing definition for value parameter" <+> quotes (pp (thing x))

      MissingModParam x ->
        "Missing module parameter" <+> quotes (pp x)

      FunctorInstanceMissingArgument i ->
        "Missing functor argument" <+> quotes (pp i)

      FunctorInstanceBadArgument i ->
        "Functor does not have parameter" <+> quotes (pp i)

      FunctorInstanceMissingName ns i ->
        "Functor argument does not define" <+> sayNS <+> "parameter" <+>
            quotes (pp i)
        where
        sayNS =
          case ns of
              NSValue     -> "value"
              NSType      -> "type"
              NSModule    -> "module"
              NSConstructor -> "constructor"

      FunctorInstanceBadBacktick bad ->
        case bad of
          BIPolymorphicArgument i x ->
            nested "Value parameter may not have a polymorphic type:" $
              bullets
                [ "Module parameter:" <+> pp i
                , "Value parameter:" <+> pp x
                , "When instantiatiating a functor using parameterization,"
                  $$ "the value parameters need to have a simple type."
                ]

          BINested what ->
            nested "Invalid declarations in parameterized instantiation:" $
              bullets $
                [ it <+> pp n
                | (w,n) <- what
                , let it = case w of
                             BIFunctor -> "functor"
                             BIInterface -> "interface"
                             BIPrimitive -> "primitive"
                             BIAbstractType -> "abstract type"
                             BIForeign -> "foreign import"
                ] ++
                [ "A functor instantiated using parameterization," $$
                  "may not contain nested functors, interfaces, or primitives."
                ]
          BIMultipleParams x ->
            nested "Repeated parameter name in parameterized instantiation:" $
              bullets
                [ "Parameter name:" <+> pp x
                , "Parameterized instantiation requires distinct parameter names"
                ]


      UnsupportedFFIKind src param k ->
        nested "Kind of type variable unsupported for FFI: " $
        vcat
          [ pp param <+> colon <+> pp k
          , "Only type variables of kind" <+> pp KNum <+> "are supported"
          , "When checking" <+> pp src ]

      UnsupportedFFIType src t -> vcat
        [ ppWithNames names t
        , "When checking" <+> pp src ]

      InvalidConstraintGuard p ->
        let d = case tNoUser p of
                  TCon tc _ -> pp tc
                  _         -> ppWithNames names p
        in
        vcat [ backticks d <+> "may not be used in a constraint guard."
             , "Constraint guards support only numeric comparisons and `fin`."
             ]

      TemporaryError doc -> doc
    where
    bullets xs = vcat [ "•" <+> d | d <- xs ]

    nested x y = nest 2 (x $$ y)

    pl 1 x     = text "1" <+> text x
    pl n x     = text (show n) <+> text x <.> text "s"

    nm x       = text "`" <.> pp x <.> text "`"

    kindMismatchHint k1 k2 =
      case (k1,k2) of
        (KType,KProp) -> [text "Possibly due to a missing `=>`"]
        _ -> []

    mismatchHint (TRec fs1) (TRec fs2) =
      hint "Missing" missing ++ hint "Unexpected" extra
      where
        missing = displayOrder fs1 \\ displayOrder fs2
        extra   = displayOrder fs2 \\ displayOrder fs1
        hint _ []  = []
        hint s [x] = [text s <+> text "field" <+> pp x]
        hint s xs  = [text s <+> text "fields" <+> commaSep (map pp xs)]
    mismatchHint _ _ = []

    noUni = Set.null (Set.filter isFreeTV (fvs err))

    ppCtxt pa = if isRootPath pa then [] else [ "Context:" <+> pp pa ]




explainUnsolvable :: NameMap -> [Goal] -> Doc
explainUnsolvable names gs =
  addTVarsDescsAfter names gs (bullets (map explain gs))

  where
  bullets xs = vcat [ "•" <+> d | d <- xs ]



  explain g =
    let useCtr = hang "Unsolvable constraint:" 2 (ppWithNames names g)

    in
    case tNoUser (goal g) of
      TCon (PC pc) ts ->
        let tys = [ backticks (ppWithNames names t) | t <- ts ]
            doc1 = case tys of
                     (doc1' : _) -> doc1'
                     [] -> error "explainUnsolvable: Expected TCon to have at least one argument"
            custom msg = hang msg
                            2 (text "arising from" $$
                               pp (goalSource g)   $$
                               text "at" <+> pp (goalRange g))
        in
        case pc of
          PEqual      -> useCtr
          PNeq        -> useCtr
          PGeq        -> useCtr
          PFin        -> useCtr
          PPrime      -> useCtr

          PHas sel ->
            custom ("Type" <+> doc1 </> "does not have field" <+> f
                    <+> "of type" <+> (tys !! 1))
            where f = case sel of
                        P.TupleSel n _ -> int n
                        P.RecordSel fl _ -> backticks (pp fl)
                        P.ListSel n _ -> int n

          PZero  ->
            custom ("Type" <+> doc1 </> "does not have `zero`")

          PLogic ->
            custom ("Type" <+> doc1 </> "does not support logical operations.")

          PRing ->
            custom ("Type" <+> doc1 </> "does not support ring operations.")

          PIntegral ->
            custom (doc1 </> "is not an integral type.")

          PField ->
            custom ("Type" <+> doc1 </> "does not support field operations.")

          PRound ->
            custom ("Type" <+> doc1 </> "does not support rounding operations.")

          PEq ->
            custom ("Type" <+> doc1 </> "does not support equality.")

          PCmp        ->
            custom ("Type" <+> doc1 </> "does not support comparisons.")

          PSignedCmp  ->
            custom ("Type" <+> doc1 </> "does not support signed comparisons.")

          PLiteral ->
            let doc2 = tys !! 1
            in custom (doc1 </> "is not a valid literal of type" <+> doc2)

          PLiteralLessThan ->
            let doc2 = tys !! 1
            in custom ("Type" <+> doc2 </> "does not contain all literals below" <+> (doc1 <> "."))

          PFLiteral ->
            case ts of
              ~[m,n,_r,_a] ->
                 let frac = backticks (ppWithNamesPrec names 4 m <> "/" <>
                                       ppWithNamesPrec names 4 n)
                     ty   = tys !! 3
                 in custom (frac </> "is not a valid literal of type" </> ty)

          PValidFloat ->
            case ts of
              ~[e,p] ->
                custom (hang "Unsupported floating point parameters:"
                           2 ("exponent =" <+> ppWithNames names e $$
                              "precision =" <+> ppWithNames names p))


          PAnd        -> useCtr
          PTrue       -> useCtr

      _ -> useCtr




-- | This picks the names to use when showing errors and warnings.
computeFreeVarNames :: PPCfg -> [(Range,Warning)] -> [(Range,Error)] -> NameMap
computeFreeVarNames cfg warns errs =
  mkMap numRoots numVaras `IntMap.union` mkMap otherRoots otherVars
    `IntMap.union` mpNames

  {- XXX: Currently we pick the names based on the unique of the variable:
     smaller uniques get an earlier name (e.g., 100 might get `a` and 200 `b`)
     This may still lead to changes in the names if the uniques got reordered
     for some reason.  A more stable approach might be to order the variables
     on their location in the error/warning, but that's quite a bit more code
     so for now we just go with the simple approximation. -}

  where
  mkName x v = (tvUnique x, text v)
  mkMap roots vs = IntMap.fromList (zipWith mkName vs (variants roots))

  (uvars,non_uvars) = partition isFreeTV
                    $ Set.toList
                    $ fvs (map snd warns, map snd errs)
        
  mpNames = computeModParamNames cfg [ tp | TVBound tp <- non_uvars ] mempty
        
  (numVaras,otherVars) = partition ((== KNum) . kindOf) uvars

  otherRoots = [ "a", "b", "c", "d" ]
  numRoots   = [ "m", "n", "u", "v" ]

  variants roots = [ nameVariant n r | n <- [ 0 .. ], r <- roots ]

